% $Id: apunte_tads_basicos.tex,v 1.2 2008-03-18 15:57:18 dbenders Exp $
\documentclass[10pt, a4paper]{article}
\usepackage[paper=a4paper, left=1.5cm, right=1.5cm, bottom=1.5cm, top=3.5cm]{geometry}
\usepackage[latin1]{inputenc}
\usepackage[T1]{fontenc}
\usepackage[spanish]{babel}
\usepackage{indentfirst}
\usepackage{fancyhdr}
\usepackage{latexsym}
%\usepackage{amssymb}
%\usepackage{lastpage}
\usepackage{aed2-symb,aed2-itef,aed2-tad}
\usepackage[colorlinks=true, linkcolor=blue]{hyperref}
\usepackage{calc}
\usepackage{caratula}
\usepackage{rcs}
%\def\sorfthanspanish{}

%\RCSdef $Revision: 2010.1 $
%\RCSdate $Date: 2010/03/09 00:00:00 $


%\newcommand{\f}[1]{\text{#1}}
%\renewcommand{\paratodo}[2]{$\forall~#2$: #1}

\sloppy

\hypersetup{%
 % Para que el PDF se abra a pgina completa.
 pdfstartview= {FitH \hypercalcbp{\paperheight-\topmargin-1in-\headheight}}
 %pdfauthor={C�tedra de Algoritmos y Estructuras de Datos II - DC - UBA},
 %pdfkeywords={TADs bsicos},
 %pdftitle={Tipos abstractos de datos b�sicos - versin \RCSRevision\ del \RCSDate},
 %pdfsubject={Tipos abstractos de datos b�sicos}
}

%\parskip=5pt % 10pt es el tamao de fuente

% Pongo en 0 la distancia extra entre temes.
%\let\olditemize\itemize
%\def\itemize{\olditemize\itemsep=0pt}

% Acomodo fancyhdr.
%\pagestyle{fancy}
%\thispagestyle{fancy}
%\addtolength{\headheight}{-25pt}
%\lhead{Trabajo Pr�ctico N$�$ 1}
%\rhead{Grupo 20}
%\cfoot{\thepage /\pageref{LastPage}}
%\renewcommand{\footrulewidth}{0.4pt}
\addtolength{\hoffset}{-0.5cm}%Para que el numero de pagina quede dentro de los margenes de impresion A4.
\addtolength{\voffset}{-1cm}%Para que el numero de pagina quede dentro de los margenes de impresion A4.

\begin{document}
%Caratula
\materia{Algoritmos y Estructuras de Datos II}
\submateria{2do Cuatrimestre de 2013}
\titulo{Trabajo Pr\'actico Nro 1}
\subtitulo{SADAIC}
%\subtituloDos{Pombo}
\grupo{Grupo Nro 4}
\integrante{Gabriel F. Quintero}{705/03}{gabrielfq@gmail.com}
%\integrante{}{}{}

%Pagina de titulo e indice
\thispagestyle{empty}

\maketitle
\tableofcontents

\newpage

\section{TAD \tadNombre{Sadaic}}

\begin{tad}{\tadNombre{SADAIC}}

\tadIgualdadObservacional{s}{s'}{sadaic}{}
\tadGeneros{sadaic}
\tadExporta{generadores, observadores, dameConjDeCatDe, pertenece?}
\tadUsa{\tadNombre{Conj($\alpha$)}, \tadNombre{Categoria}, \tadNombre{Bool}, \tadNombre{Nat}}

\ %barra \ con caracter blanco para dejar linea en blanco

\tadAlinearFunciones{arbCat}{Conj(arbolCategoria(Categoria)) cac, Categoria c}

\tadObservadores

\tadOperacion{raiz}{arbolCategoria(Categoria)}{Categoria}{}
\tadOperacion{hijos}{arbolCategoria(Categoria)}{Conj(arbolCategoria(Categoria))}{}
\ %barra \ con caracter blanco para dejar linea en blanco
%\tadAlinearFunciones{auxRecorreHijosSegunCat}{Conj(arbolCategoria(Categoria)) cac, Categoria c}
\tadGeneradores
\tadOperacion{arbCat}{Conj(arbolCategoria(Categoria))\ cac, Categoria\ c}{arbolCategoria(Categoria)}{auxSinRepetidos(cac, c)}
\ %barra \ con caracter blanco para dejar linea en blanco
\tadOtrasOperaciones
\tadAlinearFunciones{auxRecorreHijosSegunCat}{Conj(arbolCategoria(Categoria)) cac, Categoria c}
\ %barra \ con caracter blanco para dejar linea en blanco
\tadOperacion{pertenece?}{arbolCategoria(Categoria), Categoria}{Bool}{}
\tadOperacion{auxPerteneceAConj?}{Conj(arbolCategoria(Categoria)), Categoria}{Bool}{}
\tadOperacion{dameConjDeCatDe}{arbolCategoria(Categoria)\ ac, Categoria\ c}{Conj(Categoria)}{}
\tadOperacion{auxConjuntoDeRaicesDe}{Conj(arbolCategoria(Categoria))\ cac}{Conj(Categoria)}{}
\tadOperacion{auxRecorreHijosSegunCat}{Conj(arbolCategoria(Categoria))\ cac, Categoria\ c}{Conj(Categoria)}{}
\tadOperacion{auxSinRepetidos}{Conj(arbolCategoria(Categoria))\ cac, Categoria\ c}{Bool}{}
\tadOperacion{auxNodos}{Conj(arbolCategoria(Categoria))\ cac}{Nat}{}
%\tadOperacion{auxSinRepetidos}{Conj(arbolCategoria(Categoria))\ cac}{Bool}{}
%\tadOperacion{auxValidar}{multiconj(Categoria)\ m}{Bool}{}
%\tadOperacion{auxArmarMultiConj}{Conj(arbolCategoria(Categoria))\ cac}{multiconj(Categoria)}{}

\ %barra \ con caracter blanco para dejar linea en blanco
\tadAxiomas[(\paratodo{Categoria}{c}), (\paratodo{Conj(arbolCategoria(Categoria))}{cac}), (\paratodo{arbolCategoria(Categoria)}{ac})]
\ %barra \ con caracter blanco para dejar linea en blanco
\tadAlinearAxiomas{auxRecorreHijosSegunCat($cac$, $c$)}{}

\tadAxioma{raiz(arbCat($c$, $cac$))}{$c$}
\ %barra \ con caracter blanco para dejar linea en blanco
\tadAxioma{hijos(arbCat($c$, $cac$))}{$cac$}
\ %barra \ con caracter blanco para dejar linea en blanco
\tadAxioma{pertenece?($ac$, $c$)}{\IF $c$ = raiz($ac$) THEN true ELSE auxPerteneceAConj?(hijos($ac$), $c$) FI}
\ %barra \ con caracter blanco para dejar linea en blanco
\tadAxioma{auxPerteneceAConj?($cac$, $c$)}{\IF $\emptyset?$($cac$) THEN false ELSE pertenece?(dameUno($cac$), $c$) $\lor$ auxPerteneceAConj?(sinUno($cac$), $c$) FI}
\ %barra \ con caracter blanco para dejar linea en blanco 
\tadAxioma{dameConjDeCatDe($ac$, $c$)}{\IF raiz($ac$) = $c$ THEN $\{$raiz($ac$)$\}$ $\cup$ auxConjuntoDeRaicesDe(hijos($ac$)) ELSE auxRecorreHijosSegunCat(hijos($ac$), $c$) FI}{}
\ %barra \ con caracter blanco para dejar linea en blanco
\tadAxioma{auxConjuntoDeRaicesDe($cac$)}{\IF $\emptyset?$($cac$) THEN $\emptyset$ ELSE Ag(raiz(dameUno($cac$)),auxConjuntoDeRaicesDe(sinUno($cac$)))$\cup$ auxConjuntoDeRaicesDe(hijos(dameUno($cac$)))FI}{} 
%\ %barra \ con caracter blanco para dejar linea en blanco
\tadAxioma{auxRecorreHijosSegunCat($cac$, $c$)}{\IF$\emptyset?$($cac$)THEN $\emptyset$ELSE dameConjDeCatDe(dameUno($cac$),$c$)FI $\cup$ auxRecorreHijosSegunCat(sinUno($cac$), $c$)}{} 
\ %barra \ con caracter blanco para dejar linea en blanco
\tadAxioma{auxSinRepetidos($cac$, $c$)}{$\neg$auxPerteneceAConj?($cac$,$c$) $\yluego$ ($\#$auxNodos($cac$) $ = $ $\#$(auxConjuntoDeRaicesDe($cac$)))}
\ %barra \ con caracter blanco para dejar linea en blanco
\tadAxioma{$\#$auxNodos($cac$)}{\IF $\emptyset?$($cac$) THEN $0$ ELSE $1 + \#$auxNodos(sinUno($cac$)) FI $+ \#$auxNodos(hijos($cac$))}
%\tadAxioma{auxSinRepetidos($cac$)}{auxValidar(auxArmarMultiConj($cac$))}
\ %barra \ con caracter blanco para dejar linea en blanco
%\tadAxioma{auxValidar(m)}{\IF $\emptyset?$($m$) THEN true ELSE $\#$(dameUno(m), m) $= 1$ $\land$ auxValidar(sinUno(m)) FI}
\ %barra \ con caracter blanco para dejar linea en blanco
%\tadAxioma{auxArmarMultiConj(cac)}{\IF $\emptyset?$($cac$) THEN $\emptyset$ ELSE $\{$raiz(dameUno($cac$))$\}$ $\cup$ auxArmarMultiConj(hijos(dameUno($cac$))) $\cup$ auxArmarMultiConj(sinUno($cac$)) FI}
\ %barra \ con caracter blanco para dejar linea en blanco

\end{tad}

\newpage

\section{TAD \tadNombre{LinkLinkIt}}

\begin{tad}{\tadNombre{LinkLinkIt}}
\tadIgualdadObservacional{lit}{lit'}{LinkLinkIt}{categorias($lit$) \igobs categorias($lit'$)$\land$\\links($lit$) \igobs links($lit'$)$\land$\\diaDelUltimoAcceso($lit$)\igobs diaDelUltimoAcceso($lit'$)$\land$\\((\paratodo{Link}{l})($l$ $\in$ links($lit$)$\impluego$\\categoriaDeLink($lit$,$l$)$\igobs$\\categoriaDeLink($lit'$,$l$)$\land$\\(\paratodo{Dia}{d})(auxPre$\#$accesosDeLinkEnDia(lit,d) \impluego\\$\#$accesosDeLinkEnDia($lit$,$l$,$d$)\igobs $\#$accesosDeLinkEnDia($lit'$,$l$,$d$)))}

\tadGeneros{LinkLinkIt}
\tadExporta{generadores, observadores, $\#$accesosRecientesALink, categoriaDeLink}
%\tadUsa{\tadNombre{Piso}, \tadNombre{Posicion}, \tadNombre{Basura}, \tadNombre{Nat}, \tadNombre{Bool}, \tadNombre{Tupla(Nat,Nat)}, \tadNombre{Conj($\alpha$)}, \tadNombre{dicc($\alpha$,$\beta$)}}
\tadUsa{\tadNombre{arbolCategoria}, Conj($\alpha$), \tadNombre{Dia}, \tadNombre{Categoria}, \tadNombre{Link}}

\tadAlinearFunciones{$\#$accesosDeLinkEnDia}{LinkLinkIt lit, Link l, Categoria c}

\tadObservadores

\tadOperacion{categorias}{LinkLinkIt\ lit}{arbolCategoria(Categoria)}{}
\tadOperacion{links}{LinkLinkIt\ lit}{Conj(Link)}{}
\tadOperacion{diaDelUltimoAcceso}{LinkLinkIt\ lit}{Dia}{}
%\tadOperacion{diaActual}{LinkLinkIt\ lit}{Dia}{}
\tadOperacion{categoriaDeLink}{LinkLinkIt\ lit, Link\ l}{Categoria}{l $\in$ links(lit)}
\tadOperacion{$\#$accesosDeLinkEnDia}{LinkLinkIt\ lit, Link\ l, Dia\ d}{Nat}{l $\in$ links(lit) $\land$ auxPre$\#$accesosDeLinkEnDia(lit, d)}
%\tadOperacion{cuanLleno}{Oficina o, Robot r}{Nat}{r $\in$ robots(o)}
%\tadOperacion{metrosRecorridos}{Oficina o,Robot r}{Nat}{r $\in$ robots(o)}
%\tadOperacion{cuantasLlenaditas}{Oficina o,Robot r}{Nat}{r $\in$ robots(o)}

\tadAlinearFunciones{nuevoLinkLinkIt}{arbolCategoria(Categoria), Link l, Categoria c}

\tadGeneradores
\tadOperacion{nuevoLinkLinkIt}{arbolCategoria(Categoria)}{LinkLinkIt}{}
\tadOperacion{registrarLink}{LinkLinkIt\ lit, Link\ l, Categoria\ c}{LinkLinkIt}{l $\notin$ links(lit) $\land$ pertenece?(categorias(lit), c)}
\tadOperacion{accederALink}{LinkLinkIt\ lit, Link\ l, Dia\ d}{LinkLinkIt}{l $\in$ links(lit) $\land$ $d$ $\geq$ diaDelUltimoAcceso($lit$)}
%\tadOperacion{pasarDia}{LinkLinkIt}{LinkLinkIt}{}

\tadAlinearFunciones{$\#$auxAccesosRecALinkEnLos3DiasAnt}{LinkLinkIt lit, Conj(Categoria) cc, Conj(Categoria) cl}

\tadOtrasOperaciones
\ %barra \ con caracter blanco para dejar linea en blanco
%\tadOperacion{diaActual}{LinkLinkIt\ lit}{Dia}{}
\tadOperacion{$\#$accesosRecientesALink}{LinkLinkIt\ lit, Link\ l}{Nat}{l $\in$ links(lit)}
\ %barra \ con caracter blanco para dejar linea en blanco
\tadOperacion{$\#$auxAccesosRecALinkEnLos3DiasAnt}{LinkLinkIt\ lit, Link\ l, Nat\ k}{Nat}{$l$ $\in$ links($lit$) $\land$ $k \geq 0$ }
%\tadOperacion{$\#$accesosRecientesALinkEnLosDias}{LinkLinkIt\ lit, Link\ l, Conj(Dia)\ cd}{Nat}{l $\in$ links($lit$) $\wedge$ cd $\subseteq$ dias($lit$)}
\ %barra \ con caracter blanco para dejar linea en blanco
\tadOperacion{$\#$auxAccesosEnDia}{LinkLinkIt\ lit, Link\ l, Dia\ d, Dia\ dua}{Nat}{l $\in$ links(lit) $\land$ auxPre$\#$accesosDeLinkEnDia(lit,d) $\land$ dua $\geq$ $0$}
\ %barra \ con caracter blanco para dejar linea en blanco
\tadOperacion{auxPre$\#$accesosDeLinkEnDia}{LinkLinkIt\ lit, Dia\ d}{Bool}{}
\ %barra \ con caracter blanco para dejar linea en blanco
%\tadOperacion{$\#$accesosRecientesALinkEnLosDias}{LinkLinkIt\ lit, Link\ l, Conj(Dia)\ cd}{Nat}{l $\in$ links($lit$) $\wedge$ cd $\subseteq$ dias($lit$)}
%\ %barra \ con caracter blanco para dejar linea en blanco
%\tadOperacion{$\#$accesosDeLosLinksEnDia}{LinkLinkIt\ lit, Dia\ d, Conj(Link)\ cl}{Nat}{cl $\subseteq$ links($lit$) $\wedge$ d $\in$ dias($lit$)}
%\ %barra \ con caracter blanco para dejar linea en blanco
%\tadAlinearFunciones{$\#$accesosRecientesALink}{LinkLinkIt lit, Conj(Categoria) cc, Conj(Link) cl}
\ %barra \ con caracter blanco para dejar linea en blanco
\tadOperacion{$\#$linksEnCategoria}{LinkLinkIt\ lit, Categoria\ c}{Nat}{pertenece?(categorias(lit), c)}
%\ %barra \ con caracter blanco para dejar linea en blanco
%\tadOperacion{categoriasHijasDe}{LinkLinkIt\ lit, Categoria\ c}{Conj(Categoria)}{c $\in$ categorias(lit)}
\ %barra \ con caracter blanco para dejar linea en blanco
\tadOperacion{$\#$auxLinksEnCategoria}{LinkLinkIt\ lit, Conj(Categoria)\ cc, Conj(Link)\ cl}{Nat}{cl $\subseteq$ links(lit)}
%\tadOperacion{$\#$accesosRecientesEnDias}{LinkLinkIt\ lit, Link\ l, Dia\ d, Dia\ d'}{Nat}{}
%\tadOperacion{masCercanas}{Oficina o, conj(Posicion) c, Robor r}{conj(Posicion)}{c$\subseteq$posiciones(piso(o)) $\land$ r$\in$robots(o))}
%\tadOperacion{vecinasVacias}{Oficina o, Posicion p}{conj(Posicion)}{p $\in$ posiciones(piso(o))}
%\tadOperacion{filtrarVacias}{Oficina o, Posicion p, conj(Posicion) cp}{conj(Posicion)}{p $\in$ posiciones(piso(o))$\land$ cp$\subseteq$posiciones(piso(o))}
%\tadOperacion{robotElegido}{Oficina o, Posicion p}{Robot}{p $\in$ posiciones(piso(o)) $\land$ $\neg$ $\emptyset?$(robotsCandidatos(o,p,robots(o)))}
%\tadOperacion{robotsCandidatos}{Oficina o, Posicion p, conj(Robot) cr}{conj(Robot)}{p $\in$ posiciones(piso(o)) $\land$ cr $\subseteq$ robots(o) }
%\tadOperacion{posicionesSucias}{Oficina o, conj(Posicion) cp}{conj(Posicion)}{$cp$ $\subseteq$ posiciones(piso($o$))}
%\tadOperacion{posBasuraElegida}{Oficina o,Robot r}{Posicion}{r $\in$ robots(o) $\land$ $\neg\emptyset?$(posicionesConBasuraLevantable($o$,$r$))}
%\tadOperacion{basuraLevantable}{Oficina o, conj(Posicion) cp, Robot r}{conj(Posicion)}{cp$\subseteq$posiciones(piso(o)) $\land$ r $\in$ robots(o)}
%\tadOperacion{posicionElegida}{Oficina o, Robot r}{Posicion}{r $\in$ robots(o) $\land$ $\neg$(noHayBasuraLevantable($o,r$) $\land$ $\neg$($\emptyset?$(movimientosPosibles($o$,$r$))) $\land$ $\neg$vaAVaciarBolsa($o,r$)}
%\tadOperacion{habraRobot?}{Oficina o, Posicion p}{Bool}{p $\in$ posiciones(piso(o))}
%\tadOperacion{alquienQuiereMoverseAhi}{Oficina o, Posicion p, conj(Posicion) cp}{Bool}{p $\in$ posiciones(piso(o)) $\land$ cp$\subseteq$posiciones(piso(o))}
%\tadOperacion{robot}{Oficina o, Posicion p}{Robot}{($\exists$ r : Robot)($r$ $\in$ robots($o$) $\land$ posActual(o, r) = p)}
%\tadOperacion{buscarRobot}{Oficina o, conj(Robot) c, Posicion p}{Robot}{($\exists$ r : Robot)(r $\in$ robots(o) $\land$ r $\in$ c $\land$ posActual(o, r) = p)}
%\tadOperacion{posicionesConBasuraLevantable}{Oficina o, Robot r}{conj(Posicion)}{r $\in$ robots(o)} 
%\tadOperacion{filtrarLevantables}{Oficina o, conj(Posicion) c, Robot r}{conj(Posicion)}{$r$ $\in$ robots($o$) $\land$ $c\subseteq$posiciones(piso(o))}
%\tadOperacion{puedeLevantar}{Oficina o, Posicion p, Robot r}{Bool}{r $\in$ robots(o) $\land$ $p\in$posiciones($o$)}
%\tadOperacion{levantablesMasCercanas}{Oficina o, Robot r}{conj(Posicion)}{r $\in$ robots(o)} 
\ %barra \ con caracter blanco para dejar linea en blanco
\tadAxiomas[(\paratodo{LinkLinkIt}{lit}),(\paratodo{arbolCategoria(Categoria)}{ac}), (\paratodo{Link}{l,l'}), (\paratodo{Categoria}{c}), (\paratodo{Dia}{d,d',dua}), (\paratodo{Nat}{k})]
\ %barra \ con caracter blanco para dejar linea en blanco
\tadAlinearAxiomas{$\#$auxAccesosEnDia(registrarLink($lit$, $l$, $c$), $l'$, $d'$, $dua$)}{}
\tadAxioma{categorias(nuevoLinkLinkIt($ac$))}{$ac$}
\tadAxioma{categorias(registrarLink($lit$, $l$, $c$))}{categorias($lit$)}
\tadAxioma{categorias(accederLink($lit$, $l$, $d$))}{categorias($lit$)}
%\tadAxioma{categorias(pasarDia($lit$))}{categorias($lit$)}
\ %barra \ con caracter blanco para dejar linea en blanco
\tadAxioma{links(nuevoLinkLinkIt($ac$))}{$\emptyset$}
\tadAxioma{links(registrarLink($lit$, $l$, $c$))}{Ag($l$, links($lit$))}
\tadAxioma{links(accederLink($lit$, $l$, $d$))}{links($lit$)}
%\tadAxioma{links(pasarDia($lit$))}{links($lit$)}
\ %barra \ con caracter blanco para dejar linea en blanco
%\newpage
\tadAxioma{diaDelUltimoAcceso(nuevoLinkLinkIt($ac$))}{$0$}
\tadAxioma{diaDelUltimoAcceso(registrarLink($lit$, $l$, $c$))}{diaDelUltimoAcceso($lit$)}
\tadAxioma{diaDelUltimoAcceso(accederLink($lit$, $l$, $d$))}{$d$}
\ %barra \ con caracter blanco para dejar linea en blanco
\tadAxioma{categoriaDeLink(registrarLink($lit$, $l$, $c$), $l'$)}{\IF $l$ = $l'$ THEN $c$ ELSE categoriaDeLink($lit$, $l'$) FI}
\tadAxioma{categoriaDeLink(accederLink($lit$, $l$, $d$), $l'$)}{categoriaDeLink($lit$, $l'$)}
%\tadAxioma{categoriaDeLink(pasarDia($lit$), $l'$)}{categoriaDeLink($lit$, $l'$)}
\ %barra \ con caracter blanco para dejar linea en blanco
%\tadAxioma{$\#$accesosDeLinkEnDia(nuevoLinkLinkIt($ac$), $l'$, $d'$)}{$0$}
%\tadAxioma{$\#$accesosDeLinkEnDia(registrarLink($lit$, $l$, $c$), $l'$, $d$)}{\IF $d$ > diaActual($lit$) THEN $0$ ELSE {\IF $l$ = $l'$THEN $0$ ELSE $\#$accesosDeLinkEnDia($lit$, $l'$, $d$) FI} FI}
\tadAxioma{$\#$accesosDeLinkEnDia(registrarLink($lit$, $l$, $c$), $l'$, $d'$)}{\IF $l = l'$THEN$0$ ELSE $\#$accesosDeLinkEnDia($lit$, $l'$, $d$)FI}
%\tadAxioma{$\#$accesosDeLinkEnDia(accederLink($lit$, $l$, $d$), $l'$, $d'$)}{\IF $d$ = $d'$ $\land$ $l$ = $l'$ THEN $1$ ELSE 0 FI $+ \#$accesosDeLinkEnDia($lit$, $l'$, $d'$)}
\tadAxioma{$\#$accesosDeLinkEnDia(accederLink($lit$, $l$, $d$), $l'$, $d'$)}{$\#$auxAccesosEnDia(accederLink($lit$, $l$, $d$), $l'$, $d'$, diaDelUltimoAcceso(accederLink($lit$, $l$, $d$)))}
\ %barra \ con caracter blanco para dejar linea en blanco
\tadAxioma{$\#$auxAccesosEnDia(registrarLink($lit$, $l$, $c$), $l'$, $d'$, $dua$)}{\IF $l = l'$ THEN $0$ ELSE $\#$auxAccesosEnDia($lit$, $l'$, $d'$, $dua$)FI}
\tadAxioma{$\#$auxAccesosEnDia(accederLink($lit$, $l$, $d$), $l'$, $d'$, $dua$)}{\IF $dua \geq 3 \yluego d \leq dua - 3$ THEN $0$ ELSE {\IF $l = l' \land d = d'$ THEN $1$ ELSE $0$ FI} + $\#$auxAccesosEnDia($lit$, $l'$, $d'$, $dua$)FI}
%\tadAxioma{diaActual(nuevoLinkLinkIt($ac$))}{$0$}
\ %barra \ con caracter blanco para dejar linea en blanco
\tadAxioma{auxPre$\#$accesosDeLinkEnDia($lit$, $d$)}{\IF diaDelUltimoAcceso($lit$) $\geq$ $3$ THEN {\IF d $\geq$ (diaDelUltimoAcceso($lit$)$ - 3$) THEN true ELSE false FI} ELSE {\IF $0 \leq d < 3$ THEN true ELSE false FI} FI}
%\tadAxioma{diaActual(accederLink($lit$, $l$))}{diaActual($lit$)}
%\tadAxioma{diaActual(pasarDia($lit$))}{1 + diaActual($lit$)}
%\tadAxioma{basuraLimpiada? ($o$,$p$)}{habraRobot?($o$,$p$) $\land$ puedeLevantar($o$,robotElegido($o$,$p$),$p$)}
\ %barra \ con caracter blanco para dejar linea en blanco $\#$accesosDeLinkEnDia

%\tadAxioma{dias(pasarDia($lit$))}{Ag(diaActual($lit$), dias($lit$))}
%\ %barra \ con caracter blanco para dejar linea en blanco $\#$accesosDeLinkEnDia
\ %barra \ con caracter blanco para dejar linea en blanco
%\tadAxioma{$\#$accesosRecientesALink($lit$, $l$)}{$\#$accesosRecientesALinkEnLosDias($lit$,$l$, $\#$auxAccesosRecientesALinkEnLos3DiasAnteriores($lit$, $l$, $0$)}
\tadAxioma{$\#$accesosRecientesALink($lit$, $l$)}{$\#$auxAccesosRecALinkEnLos3DiasAnt($lit$, $l$, $0$)}
\ %barra \ con caracter blanco para dejar linea en blanco
%\tadAxioma{$\#$accesosRecientesALinkEnLosDias($lit$, $l$, $cdr$)}{\IF $\emptyset?$($cdr$) THEN $0$ ELSE $\#$accesosRecientesALinkEnLosDias($lit$,$l$,dameUno($cdr$))FI + $\#$accesosRecientesALinkEnLosDias($lit$, $l$, sinUno($cdr$))}
\tadAxioma{$\#$auxAccesosRecALinkEnLos3DiasAnt($lit$, $l$, $k$)}{\IF ($k$ $\geq$ 3) $\lor$ ($k$ $\leq$ diaDelUltimoAcceso($lit$) $\yluego$ diaDelUltimoAcceso($lit$) $-$ $k$ $<$ $0$) THEN $0$ ELSE $\#$accesosDeLinkEnDia($lit$,$l$, diaDelUltimoAcceso($lit$)$ - k$) $+ \#$auxAccesosRecALinkEnLos3DiasAnt($lit$, $l$, $k + 1$) FI}
%\ %barra \ con caracter blanco para dejar linea en blanco
%\tadAxioma{dameConjDeLosKDiasMenoresIgualesA($cd$,$k$)}{\IF $\emptyset?$($cd$) $\lor$ $k = 0$ THEN $\emptyset$ ELSE $\{$dameMaxDia($cd$)$\}$ $\cup$ dameConjDeLosKDiasMenoresIgualesA($cd$ $-$ $\{$dameMaxDia($cd$)$\}$, $k - 1$) FI} 
%\ %barra \ con caracter blanco para dejar linea en blanco
%\tadAxioma{diaDelUltimoAcceso($lit$, $cd$)}{\IF $\emptyset?$($cd$) THEN $0$ ELSE {\IF $\#$accesosDeLosLinksEnDia($lit$, dameMaxDia($cd$), links($lit$)) > $0$ THEN dameMaxDia($cd$) ELSE diaDelUltimoAcceso($lit$, $cd$ $-$ $\{$dameMaxDia($cd$)$\}$) FI} FI}
%\ %barra \ con caracter blanco para dejar linea en blanco
%\tadAxioma{$\#$accesosDeLosLinksEnDia($lit$, $da$, $cl$))}{\IF $\emptyset?$($cl$) THEN $0$ ELSE $\#$accesosDeLinkEnDia($lit$,dameUno($cl$),$da$) + \\ $\#$accesosDeLosLinksEnDia($lit$, $da$, sinUno($cl$)) FI}
%\ %barra \ con caracter blanco para dejar linea en blanco
%\tadAxioma{dameMaxDia($cd$)}{\IF $\emptyset?$($cd$) THEN $0$ ELSE max(dameUno($cd$), dameMaxDia(sinUno($cd$))) FI}
\ %barra \ con caracter blanco para dejar linea en blanco
%\tadAxioma{$\#$accesosRecientesALink(nuevoLinkLinkIt($ac$),$l'$)}{$0$}
%\tadAxioma{$\#$accesosRecientesALink(registrarLink($lit$, $l$, $c$), $l'$)}{accesosRecientesALink($lit$, $l'$)}
%\tadAxioma{$\#$accesosRecientesALink(accederLink($lit$, $l$), $l'$)}{\IF diaActual($lit$) $>$ diaUltimoAcceso($lit$)-3 $\land$ $l$ = $l'$ THEN $1$ ELSE 0 FI + $\#$accesosRecientesALink($lit$,$l'$)}
%\tadAxioma{$\#$accesosRecientesALink(pasarDia($lit$), $l'$)}{$\#$accesosRecientesALink($lit$, $l'$)} 
%\tadAxioma{$\#$accesosRecientesALink($lit$, $l$)}{$\#$accesosRecientesEnDias($lit$, $l$, diaDelUltimoAcceso($lit$, diaActual($lit$)), diaActual($lit$))}
\ %barra \ con caracter blanco para dejar linea en blanco
%\tadAxioma{$\#$accesosRecientesEnDias($lit$, $l$, $dua$, $ddec$)}{\IF ($dua$ $-$ 3 $>$ $ddec$) $\land$ (ddec $\geq$ $0$) THEN $0$ ELSE $\#$accesosDeLinkEnDia($lit$, $l$, $ddec$) FI + $\#$accesosRecientesEnDias($lit$, $l$, $dua$, $ddec$ $-$ 1)}
\ %barra \ con caracter blanco para dejar linea en blanco
%\tadAxioma{$\#$linksEnCategoria(nuevoLinkLinkIt($ac$),$c'$)}{$0$}
%\tadAxioma{$\#$linksEnCategoria(registrarLink($lit$, $l$, $c$), $c'$)}{\IF $c$ $\in$ dameConjDeCatDe(categorias($lit$),$c'$) THEN $1$ ELSE 0 FI + $\#$linksEnCategoria($lit$, $c'$)}
%\tadAxioma{$\#$linksEnCategoria(accederLink($lit$, $l$), $c'$)}{$\#$linksEnCategoria($lit$, $c'$)}
%\tadAxioma{$\#$linksEnCategoria(pasarDia($lit$), $c'$)}{$\#$linksEnCategoria($lit$, $c'$)} 
\ %barra \ con caracter blanco para dejar linea en blanco
\ %barra \ con caracter blanco para dejar linea en blanco
\tadAxioma{$\#$linksEnCategoria($lit$, $c$)}{$\#$auxLinksEnCategoria($lit$, dameConjDeCatDe(categorias($lit$), $c$), links($lit$))}
\ %barra \ con caracter blanco para dejar linea en blanco
%\tadAxioma{$\#$auxLinksEnCategoria($lit$, $cc$, $cl$)}{\IF $\emptyset?$($cl$) $\yluego$ (categoriaDeLink($lit$ , dameUno($cl$)) $\in$ $cl$) THEN $1 + $ $\#$auxLinksEnCategoria($lit$, $cc$, sinUno($cl$)) ELSE $0$ FI}
\tadAxioma{$\#$auxLinksEnCategoria($lit$, $cc$, $cl$)}{\IF $\emptyset?$($cl$) THEN $0$ ELSE {\IF categoriaDeLink($lit$ , dameUno($cl$)) $\in$ $cc$ THEN $1$ ELSE $0$ FI}$+ \#$auxLinksEnCategoria($lit$, $cc$, sinUno($cl$)) FI}
\ %barra \ con caracter blanco para dejar linea en blanco
%\tadAxioma{cuanLleno(nuevaOficina($t$, $pyb$, $dr$),r)}{0}
%\tadAxioma{cuanLleno(nuevoGong($o$),$r$)}{\IF vaAVaciarBolsa($o$,$r$) THEN 0 ELSE {
%\IF $\neg$noSeMovio($o$,$r$) $\wedge$ puedeLevantar($o$,posicionElegida($o$,$r$),$r$) THEN $\#$basuraActual($o$,posicionElegida($o$,$r$)) ELSE 0 FI} + cuanLleno($o$,$r$)
%FI}       
\ %barra \ con caracter blanco para dejar linea en blanco
%\tadAxioma{noSeMovio ($o$, $r$)}{vaAVaciarBolsa($o$, $r$) $\lor$ noHayBasuraLevantable($o$,$r$) $\lor$ $\emptyset?$(movimientosPosibles($o$,$r$)) $\lor$ noPudoMoverse($o$, $r$)}
\ %barra \ con caracter blanco para dejar linea en blanco
%\tadAxioma{posActual (nuevaOficina($t, pyb, dr$),$r$)}{$\Pi_1$(obtener($r$,$dr$))}
%\tadAxioma{posActual (nuevoGong($o$),$r$)}{\IF noSeMovio($o$,$r$) THEN posActual($o$,$r$) ELSE posicionElegida($o$,$r$) FI}
\ %barra \ con caracter blanco para dejar linea en blanco
%\tadAxioma{vaAVaciarBolsa ($o$,$r$)}{(capacidad($o$,$r$) - cuanLleno($o$,$r$)) = $\#$basuraActual($o$,posActual($o$,$r$))}
\ %barra \ con caracter blanco para dejar linea en blanco
%\tadAxioma{noPudoMoverse ($o$,$r$)}{robotElegido($o$, posicionElegida($o$,$r$)) $\neq$ $r$}
\ %barra \ con caracter blanco para dejar linea en blanco
%\tadAxioma{capacidad (nuevaOficina($t, pyb, dr$),$r$)}{$\Pi_2$(obtener($r$,$dr$))}
%\tadAxioma{capacidad (nuevoGong($o$),$r$)}{capacidad($o$,$r$)}
\ %barra \ con caracter blanco para dejar linea en blanco
%\tadAxioma{metrosRecorridos (nuevaOficina($t, pyb, dr$),$r$)}{$0$}
%\tadAxioma{metrosRecorridos (nuevoGong($o$),$r$)}{\IF $\neg$noSeMovio($o$,$r$) THEN 1 $+$ metrosRecorridos($o$,$r$) ELSE metrosRecorridos($o$,$r$) FI}
\ %barra \ con caracter blanco para dejar linea en blanco
%\tadAxioma{cuantasLlenaditas (nuevaOficina($t, pyb, dr$),$r$)}{$0$}
%\tadAxioma{cuantasLlenaditas (nuevoGong($o$),$r$)}{\IF cuanLleno($o$,$r$) = capacidad($o$,$r$) THEN 1 $+$ cuantasLlenaditas($o$,$r$) ELSE cuantasLlenaditas($o$,$r$) FI}
\ %barra \ con caracter blanco para dejar linea en blanco
%\tadAxioma{hayRobot? ($o$,$p$)}{$p$ $\in$ posicionesActuales($o$,robots($o$))}
\ %barra \ con caracter blanco para dejar linea en blanco
%\tadAxioma{posicionesActuales ($o$,$cr$)}{\IF $\emptyset?$($cr$) THEN $\emptyset$ ELSE Ag(posActual($o$,dameUno($cr$)), posicionesActuales(sinUno($cr$))) FI}
\ %barra \ con caracter blanco para dejar linea en blanco
%\tadAxioma{noHayBasuraLevantable ($o$,$r$)}{$\emptyset?$(basuraLevantable($o$,posicionesSucias($o$,posiciones(piso($o$))),$r$))}
\ %barra \ con caracter blanco para dejar linea en blanco
%\tadAxioma{movimientosPosibles($o$,$r$)}{masCercanas($o$,vecinasVacias($o$,$p$),$r$)}
%\tadAxioma{masCercanas($o$,$c$,$r$)}{
%\IF $\emptyset?$($c$) THEN $\emptyset$ ELSE {\IF meAcerca(piso($o$),dameUno($c$),posActual($o$,$r$),posBasuraElegida($o$,$r$)) THEN Ag(dameUno(c),masCercanas(o,sinUno(c),r)) ELSE masCercanas(o,sinUno(c),r) FI} FI }
\ %barra \ con caracter blanco para dejar linea en blanco
%\tadAxioma{vecinasVacias($o$,$p$)}{filtrarVacias($o$,$p$,vecinas(piso($o$),$p$))}
\ %barra \ con caracter blanco para dejar linea en blanco
%\tadAxioma{filtrarVacias($o$,$p$,$cp$)}{\IF $\emptyset?$($cp$) THEN $\emptyset$ ELSE {\IF $\neg$(hayRobot?($o$,dameUno($cp$))) THEN Ag(dameUno($cp$),filtrarVacias($o$,$p$,sinUno($cp$))) ELSE filtrarVacias($o$,$p$,sinUno($cp$)) FI} FI}
\ %barra \ con caracter blanco para dejar linea en blanco
%\tadAxioma{robotElegido($o$,$p$)}{dameUno(robotsCandidatos($o$,$p$,robots($o$)))}
\ %barra \ con caracter blanco para dejar linea en blanco
%\tadAxioma{robotsCandidatos($o$,$p$,$cr$)}{\IF $\emptyset?$($cr$) THEN $\emptyset$ ELSE {\IF ($\neg$vaAVaciarBolsa($o$,dameUno($cr$)) $\wedge$ $\neg$(noHayBasuraLevantable($o,r$)) $\wedge$ $\neg$($\emptyset?$(movimientosPosibles($o$,dameUno($cr$)))) $\wedge$ posBasuraElegida($o$, dameUno($cr$))=$p$) \\THEN Ag(dameUno($cp$), robotsCandidatos($o$,$p$,sinUno($cr$))) ELSE robotsCandidatos($o$,$p$,sinUno($cr$))FI} FI}
\ %barra \ con caracter blanco para dejar linea en blanco
%\tadAxioma{posicionesSucias($o$,$cp$)}{\IF $\emptyset?$($cp$) THEN $\emptyset$ ELSE {\IF $\#$basuraActual($o$,dameUno($cp$))>0 THEN Ag(dameUno($cp$),posicionesSucias($o$,sinUno($cp$))) ELSE posicionesSucias($o$,sinUno($cp$)) FI} FI}
\ %barra \ con caracter blanco para dejar linea en blanco
%\tadAxioma{posBasuraElegida($o$,$r$)}{dameUno(levantablesMasCercanas($o$,$r$))} 
\ %barra \ con caracter blanco para dejar linea en blanco
%\tadAxioma{basuraLevantable($o$,$cp$,$r$)}{\IF puedeLevantar($o$,$r$,dameUno($cp$) THEN Ag(dameUno($cp$),$\emptyset$)$\cup$ basuraLevantable($o$,sinUno($cp$),$r$) ELSE basuraLevantable($o$,sinUno($cp$),$r$) FI}
\ %barra \ con caracter blanco para dejar linea en blanco
%\tadAxioma{posicionElegida($o$,$r$)}{dameUno(movimientosPosibles($o$,$r$))}
\ %barra \ con caracter blanco para dejar linea en blanco
%\tadAxioma{posicionesConBasuraLevantable($o$,$r$)}{filtrarLevantables(o,posicionesSucias(o),r)}
\ %barra \ con caracter blanco para dejar linea en blanco
%\tadAxioma{filtrarLevantables(o, cp, r)}{\IF $\emptyset?$($cp$) THEN $\emptyset$ ELSE 
%{\IF puedeLevantar( $o$, dameUno($cp$) ,$r$) THEN  Ag( dameUno($cp$), filtrarLevantables($o$, sinUno($cp$) , $r$)
%ELSE filtrarLevantables($o$, sinUno($cp$) , $r$) FI}
%FI}
\ %barra \ con caracter blanco para dejar linea en blanco
%\tadAxioma{puedeLevantar(o,p,r)}{(capacidad($o$,$r$) - cuanLleno($o$,$r$)) $\geq$ $\#$basuraActual($o$,$p$)}
\ %barra \ con caracter blanco para dejar linea en blanco
%\tadAxioma{levantablesMasCercanas($o$,$r$)}{filtrarPorDistancia( piso($o$), posicionesConBasuraLevantable($o$,$r$), 
%minimaDistancia(piso($o$), posicionesConBasuraLevantable($o$,$r$), posActual($o$,$r$)),
%posActual(o,r) )}
\end{tad}


%\newpage
%\section{ \tadNombre{Operaciones Auxiliares}}
%\subsection{Signatura}
%\ %barra \ con caracter blanco para dejar linea en blanco
%\tadOperacion{max}{Nat n, Nat m}{Nat}{}
%\tadOperacion{min}{Nat n, Nat m}{Nat}{}
%\tadOperacion{distX}{Nat, Nat}{Nat}{}
%\tadOperacion{distY}{Nat, Nat}{Nat}{}
%\tadOperacion{generarPosiciones}{Nat, Nat}{conj(Posicion)}{}
%\tadOperacion{agregarFila}{Nat, Nat}{conj(Posicion)}{}
%%%%%\tadOperacion{mirarDic}{Posicion p, dicc(Robot{,} Tupla(Posicion{,} Capacidad)) dr}{Bool}{}

%\subsection{Axiomas}
%\ %barra \ con caracter blanco para dejar linea en blanco
%\tadAxioma{max(n,m)}{\IF n $\geq$ m THEN n ELSE m FI}{}
%\ %barra \ con caracter blanco para dejar linea en blanco
%\tadAxioma{min(n,m)}{\IF n $\leq$ m THEN n ELSE m FI}{}
%\ %barra \ con caracter blanco para dejar linea en blanco
%\tadAxioma{distX(n,m)}{max(n,m) - min(n,m)}{}
%\ %barra \ con caracter blanco para dejar linea en blanco
%\tadAxioma{distY(n,m)}{max(n,m) - min(n,m)}{}
%\ %barra \ con caracter blanco para dejar linea en blanco
%\tadAxioma{generarPosiciones(x, y)}{\IF x $\geq$ 1 THEN agregarFila(x, y) $\cup$ generarPosiciones(x - 1, y) ELSE $\emptyset$ FI}
%\ %barra \ con caracter blanco para dejar linea en blanco
%\tadAxioma{agregarFila(x, y)}{\IF y $\geq$ 1 THEN Ag((x - 1, y - 1), agregarFila(x, y - 1)) ELSE $\emptyset$ FI}
%\ %barra \ con caracter blanco para dejar linea en blanco
%%%%\tadAxioma{mirarDic ($p$, $dr$)}{\IF $\emptyset?$(claves($dr$)) THEN false ELSE {\IF $\Pi_1$(obtener(dameUno(claves($dr$)),$dr$)) = $p$ THEN true ELSE mirarDic(borrar(dameUno(claves($dr$),$dr$))) FI} FI}
%\tadOperacion{buscarMovimientos}{Piso t, conj(flecha) cf, casillero c}{conj(movimiento)}{cf$\subseteq$flechas(t) $\land$ c$\in$casilleros(t)}
%\tadAxioma{buscarMovimientos($cf$,$c$)}{\IF $\emptyset?(cf)$ THEN $\emptyset$ ELSE {\IF origen(dameUno$(cf)$)=c THEN 
%Ag(movimiento(dameUno$(cf)$),buscarMovimientos(sinUno$(cf)$,$c$)) ELSE buscarMovimientos(sinUno$(cf)$,$c$) FI} FI}{}

\begin{quote}
TAD \textbf{Categoria} es \textbf{String}\\
TAD \textbf{Link} es \textbf{String}\\
TAD \textbf{Dia} es \textbf{Nat}\\
%TAD \textbf{Posicion} es \textbf{Tupla<X: Nat,Y: Nat>}\\
%TAD \textbf{Robot} es \textbf{Nat}\\
%TAD \textbf{Flecha} es \textbf{Tupla<origen:casillero, destino:casillero, movimiento: movimiento >}\\

\end{quote}
\newpage

\section{ \tadNombre{Decisiones tomadas:}}
%\parindent=1cm
%\parskip=0.5cm
\begin{quote}
\ \ \ En l\'ineas generales s\'olo quisi\'eramos comentar las siguientes decisiones tomadas:
\ \ \ \ \ \ \paragraph{\ \ \ $\bullet$ TAD: ArbolCategoria}
%\parindent=1cm
%\parskip=0.5cm
\begin{verse}
1) Al principio intentamos utilizar el TAD RoseTree($\alpha$) del ejercicio 6 de la pr\'actica 1 para construir el TAD ArbolCategoria, pero despu\'es notamos que el TAD RoseTree($\alpha$) almacena los hijos de un nodo en una secuencia.
Al estar implementado con una secuencia, los nodos est\'an ordenados y para el \'arbol de categor\'ias no necesit\'abamos que dichos nodos estuvieran ordenados. 
Debido a esto, nos pareci\'o mejor idea hacer un TAD similar al RoseTree($\alpha$) pero usando un conjunto en lugar de una secuencia.
\end{verse}
\begin{verse}
2) Para implementar las funciones perteneceAConj y dameConjDeCatDe fue necesario hacer recursi\'on mutua entre cada una de estas funciones y sus respectivas auxiliares. 
Esto se debe a que ArbolCategoria es muy similar a un RoseTree y cada nodo no tiene limitado el n\'umero de hijos.
\end{verse}
%\paragraph{$\bullet$ $\#$basuraActual en instancia NuevaOficina:} 
%Elegimos, entendiendo que la acci\'on de limpiar posici\'on es autom\'atica, que una posici\'on donde haya robot y basura que el robot pueda levantar, est\'e *limpia* (aunque todav\'ia no hayan sucedido gongs). 
\end{quote}
\begin{quote}
\ \ \ \ \ \ \ \paragraph{\ \ \ $\bullet$ TAD: LinkLinkIt}
%\parindent=1cm
%\parskip=0.5cm
%\parindent=1cm
\begin{verse}
1) Nos pareci\'o mejor y m\'as acorde con el enunciado del trabajo pr\'actico, tomar como observador b\'asico el d\'ia del \'ultimo acceso al sistema y no registrar el paso del tiempo.
Dado que en el enunciado aclara que solo interesan los \'ultimos 3 d\'ias anteriores al d\'ia del \'ultimo acceso.
\end{verse}

\begin{verse}
2) Otro detalle importante es que, solo se puede acceder a los links en dias mayores o iguales al dia actual.
\end{verse}

\begin{verse} 
3) El observador b\'asico diaDelUltimoAcceso devuelve 0, tanto en el caso de que existan accesos a alg\'un link en el dia cero como en el caso de que nunca se haya accedido a ning\'un link.
%El dia cero es usado unicamente cuando se pide el diaDelUltimoAcceso al generador nuevoLinkLinkIt, debido a esto los dias van del 1 en adelante. 
\end{verse}

\begin{verse}
4) Los nombres son nombres largos y muy descriptivos, debido a que se intent\'o hacer que el nombre de la funci\'on sea lo mas declarativo posible, por otro lado, todas las funciones que tengan ``aux'' como prefijo son funciones auxiliares.
\end{verse}

\end{quote}

%\newpage
%\section{ \tadNombre{Agregado en Oficina}}
%\subsection{Otras Operaciones}
%\tadOperacion{laQueMasBasuraRecolecto}{Oficina o}{Robot}{$\neg$($\emptyset?$(robots(o)))}
%\tadOperacion{maxLlenadita}{Oficina o, conj(Robot)cr}{Nat}{$\neg$($\emptyset?$(cr))}
%\tadOperacion{mayoresLlenaditas}{Oficina o, conj(Robot)cr, Nat n}{conj(Robot)}{cr$\subseteq$robots(o)}
%\tadOperacion{losMasLlenos}{Oficina o, conj(Robot)cr, Nat n}{conj(Robot)}{cr$\subseteq$robots(o)}
%\tadOperacion{cantBasuraMaxima}{Oficina o, conj(Robot)cr}{Nat}{$\neg$($\emptyset?$(cr))}
%\tadOperacion{laQueMasBasuraRecolecto}{Oficina o}{Robot}{$\neg$($\emptyset?$(robots(o)))}

%\ %barra \ con caracter blanco para dejar linea en blanco
%\tadOperacion{laQueMasBasuraRecolecto}{Oficina o}{Robot}{$\neg$($\emptyset?$(robots(o)))}
%\ %barra \ con caracter blanco para dejar linea en blanco
%\tadOperacion{lasMasLlenas}{Oficina o}{Conj(Robot)}{}
%\ %barra \ con caracter blanco para dejar linea en blanco
%\tadOperacion{filtrarPorCuanLleno}{Oficina o, Conj(Robot) cr, Nat n}{Conj(Robot)}{cr $\subseteq$ robots(o)}
%\ %barra \ con caracter blanco para dejar linea en blanco
%\tadOperacion{conMasLlenaditas}{Oficina o}{Conj(Robot)}{}
%\ %barra \ con caracter blanco para dejar linea en blanco
%\tadOperacion{filtrarPorCuantasLlenaditas}{Oficina o, Conj(Robot) cr, Nat n}{Conj(Robot)}{cr $\subseteq$ robots(o)}
%\ %barra \ con caracter blanco para dejar linea en blanco
%\tadOperacion{mayorCantBasura}{Oficina o, conj(Robot) cr}{Nat}{cr $\subseteq$ robots(o) $\land$ $\neg$($\emptyset?$(cr))}
%\ %barra \ con caracter blanco para dejar linea en blanco
%\tadOperacion{maxLlenadita}{Oficina o, conj(Robot) cr}{Nat}{cr $\subseteq$ robots(o) $\land$ $\neg$($\emptyset?$(cr))}
%\ %barra \ con caracter blanco para dejar linea en blanco
%\subsection{Axiomas}

%\tadAxioma{laQueMasBasuraRecolecto(o)}{dameUno(losMasLlenos(o,\\mayoresLlenaditas(o,robots(o),maxLlenadita(o,robots(o))), \\cantBasuraMaxima(o,mayoresLlenaditas(o,robots(o),maxLlenadita(o,robots(o))))))}{}
%\tadAxioma{maxLlenadita(o, cr)}{\IF $\#$(cr)=1 THEN cuantasLlenaditas(o,dameUno(cr)) ELSE max(cuantasLlenaditas(o,dameUno(cr)), maxLlenadita(o,sinUno(cr))) FI}{}
%\tadAxioma{mayoresLlenaditas(o, cr, n)}{\IF $\emptyset?$(cr) THEN $\emptyset$ ELSE {\IF cuantasLlenaditas(o,dameUno(cr))< n THEN mayoresLlenaditas(o,sinUno(cr),n) ELSE Ag(dameUno(cr), mayoresLlenaditas(o,sinUno(cr),n)) FI} FI}{}
%\tadAxioma{losMasLlenos(o ,cr, n)}{\IF $\emptyset?$(cr) THEN $\emptyset$ ELSE {\IF cuanLleno(o,dameUno(cr))< n THEN losMasLlenos(o, sinUno(cr), n) ELSE Ag(dameUno(c), losMasLlenos(o, sinUno(cr), n)) FI} FI}{}
%\tadAxioma{cantBasuraMaxima(o ,cr)}{\IF $\#$(cr)=1 THEN cuanLleno(o, dameUno(cr)) ELSE max(cuanLleno(o, dameUno(cr)),cantBasuraMaxima(o, sinUno(cr))) FI}{}
%\ %barra \ con caracter blanco para dejar linea en blanco
%\tadAxioma{laQueMasBasuraRecolecto(o)}{dameUno(lasMasLlenas(o))}{}
%\ %barra \ con caracter blanco para dejar linea en blanco
%\tadAxioma{lasMasLlenas(o)}{filtrarPorCuanLleno(o, conMasLlenaditas(o), mayorCantBasura(o,conMasLlenaditas(o)))}{}
%\ %barra \ con caracter blanco para dejar linea en blanco
%\tadAxioma{filtrarPorCuanLleno(o, cr, n)}{\IF $\emptyset?$(cr) THEN $\emptyset$ ELSE {\IF cuanLleno(o,dameUno(cr))< n THEN filtrarPorCuanLleno(o,sinUno(cr),n) ELSE Ag(dameUno(cr), filtrarPorCuanLleno(o,sinUno(cr),n)) FI} FI}{}
%\ %barra \ con caracter blanco para dejar linea en blanco
%\tadAxioma{conMasLlenaditas(o)}{filtrarPorCuantasLlenaditas(o,robots(o),maxLlenadita(o,robots(o)))}{}
%\ %barra \ con caracter blanco para dejar linea en blanco
%\tadAxioma{filtrarPorCuantasLlenaditas(o, cr, n)}{\IF $\emptyset?$(cr) THEN $\emptyset$ ELSE {\IF cuantasLlenaditas(o,dameUno(cr))< n THEN filtrarPorCuantasLlenaditas(o, sinUno(cr), n) ELSE Ag(dameUno(c), filtrarPorCuantasLlenaditas(o, sinUno(cr), n)) FI} FI}{}
%\ %barra \ con caracter blanco para dejar linea en blanco
%\tadAxioma{mayorCantBasura(o ,cr)}{\IF $\#$(cr)=1 THEN cuanLleno(o, dameUno(cr)) ELSE max(cuanLleno(o, dameUno(cr)),mayorCantBasura(o, sinUno(cr))) FI}{}
%\ %barra \ con caracter blanco para dejar linea en blanco
%\tadAxioma{maxLlenadita(o, cr)}{\IF $\#$(cr)=1 THEN cuantasLlenaditas(o,dameUno(cr)) ELSE max(cuantasLlenaditas(o,dameUno(cr)), maxLlenadita(o,sinUno(cr))) FI}{}
%\ %barra \ con caracter blanco para dejar linea en blanco
\end{document}
